Learning to Discover Interesting Mathematics
学习发现有趣的数学定理
🧭 LLM 数学定理发现 · 形式化证明库
FAIR @ Meta · New York University · CERMICS, ENPC, Institut Polytechnique de Paris
定义证明长度/陈述长度比作为定理有趣度代理，训练27B模型预测证明难度并用于自扩展数学库
📌 工作参考价值（4 点）
- 轻量代理指标设计：在业务中可类比“信息密度/交互深度”定义内在质量分（如 query 长度 vs 后续点击/转化链长度），训练低成本打分模型替代大模型或人工标注，用于候选排序。
- 中等规模 reward/scorer 模型：27B 即可超过 frontier 通用模型，说明特定领域可训小模型做难度/效用预测，降低线上打分成本，适合广告创意/商品文案候选筛选。
- 自扩展库 + 去重过滤：生成候选后按指标选择并过滤与已有库高重叠项，从 91.9% 降到 30.6%，可借鉴到推荐/广告生成场景，避免生成结果与历史素材同质化。
- 迭代构建优质候选池：以自扩展方式逐步加入经证明有效/有趣的候选，可迁移到 query 推荐、push 文案库的自动扩量。